COMMENT ⊗   VALID 00012 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	
 00004 00003	.NEXT PAGE
 00009 00004	.NEXT PAGE
 00012 00005	.NEXT PAGE
 00014 00006	.NEXT PAGE 
 00019 00007	
 00020 00008	THE INPUT FORMAT
 00024 00009	
 00026 00010	.NEXT PAGE
 00028 00011	
 00030 00012	.NEXT PAGE
 00031 ENDMK
⊗;

.BEGIN DOUBLE SPACE
Frequently the user of a theorem prover "knows" a lot of detail
about the problem domain being axiomatized.  Much of this information
(almost by definiton) is domain-dependent and  thus doesn't fit the 
usual set of strategies as well as could be desired. Also much of this
information is heuristic in nature  and would be difficlut to express
in the form of axioms.
To help with these problems we have introduced two new ideas: (1) a language
for describing strategies; and (2) new data types have been added to LISP
so that the user may tailor-make his own prover.

The strategy language allows Boolean expressions over properties
of clauses.  Major extensions of this idea are contemplated..

The programmable aspects allow the user to describe  first order statements, strategies
and pattern matching in an intuitive notation. With these facilities inside LISP
we can write new rules of inference and domain dependent theorem provers.

.NEXT PAGE
VIII. The Language of Strategies.


(1) Choice strategies.

Choice strategies occur in the following context: Given two  possible
candidates,C1 and C2, for the application of a binary rule of inference,
I, a choice strategy will determine whether not we wish to form I(C1,C2).

Builtin choice strategies.

a) NONE  allows unrestricted applications of the rules of inference.

b) ANCESTRY implements the AFF strategy; that is, to apply I either C1 or
C2 must be an initial clauses, or, either C1 appears in the derivation tree
of C2, or C2 appears in the tree of C1.

c) SUPPORT designates the set-of-support strategy. This strategy basically says 
that every first-level deduction must have one of its parents in the
support set.  SUPPORT must be followed
by an argument list describing which  statements are to be supported.
The elements of the argument list may either be clause numbers or names
which the user has associated with certain input clauses.

Example: SUPPORT[1,2,AXIOM[2],THEOREM] would put clauses numbered 1 and 2, the 
clause AXIOM[2], and all clauses with name, THEOREM, in the support set.


d) VINE strategy says that either C1 or C2 must be an initial clause.  This 
strategy is known to be incomplete, but is useful in many cases. 

e) UNIT strategy says that either C1 or C2 are singletons.  Again, this strategy
is not complete ,but is useful as a "quick-kill" or "end-game" strategy.
It is easy to show that if there is a UNIT-refutation then there is a VINE-form
refutation. It is also easy to show that if all the initial statements are either
units(singletons) or are of the form L1∧L2∧...∧Ln ⊃ M then there is a UNIT 
proof.


f) P1 is the P1-deduction of Robinson. Here it is required that either
C1 or C2 contain only positive literals. This strategy is complete.


g) MODEL is the implementation of a very simple  case of the model-relative 
deduction strategy of Luckham.  Model-relative deduction is a generalization
of P1 deduction and is complete.  Deduction relative to a model says
that at least one of the clauses C1 or C2 be false of the model.  MODEL expects 
an argument list describing a binary partition of the predicate letters appearing
in the initial clauses. In the current restricted implementation this says either C1
or C2 must have zero intersection with the two members of the partition.


h) DEFMODEL can be used to designate a LISP function to define a model for the
current set of statements.  DEFMODEL expects a single argument which is the name
of a LISP function(of one argument) and which implements the defining conditions
of a model.


i) EQUALITY signals that the replacement rule, paramodulation, is to be used.
EQUALITY needs two arguments: a predicate name to be interpreted as equality;
and second, a number, called PDEPTH, which determines how deep in the nesting
of function symbols the matcher will look in attempting to match terms.
For example, a PDEPTH of 1 says only examine primary occurences of terms.


.NEXT PAGE

(2) Editing Strategies.


Editing strategies are applied to the results of the rules of inference.
These strategies are used to  filter out some of the deductions which a rule
of inference has generated.

Builtin editing strategies.

a) DEMOD is a rule of simplification most commonly used in conjunction with
EQUALITY. DEMOD takes two arguments. The first describes a list of equality units;
the second, a number named DDEPTH which,like PDEPTH, determines a bound on the
matching routines.


b) DEPTH takes a single integer argument interpreted to be a bound on the depth of
function symbol nesting which must not be exceeded if the deduction is to be retained.

For example, DEPTH[4].

c) LENGTH also takes an integer argument and gives a bound on the number of literals
which will be allowed in any deduction.

d) SELDEPTH takes function symbol-number pairs as arguments.  SELDEPTH is a refinement
of DEPTH in that the allowable depth of nesting of each function symbol is determined
by the corresponding number.

e) Any of the primitive constructs of the pattern language: TREE, LENGTH, DEPTH, or
OCR.  For example if OCR[f(e,e)] were to appear in an editing strategy then any
clauses which contained "f(e,e)" would be rejected.
.NEXT PAGE

Boolean combinations of built-in or user-defined strategies are allowed.
For example, a reasonable choice strategy  is: ancestry filter form
with a set of support being the negation of the statement to be proved.
This can be written as:

 ANCESTRY ∧ SUPPORT[THEOREM];


An editing strategy which filters out all clauses whose length(number of literals)
is greater than 4 or whose depth( depth of nesting of function symbols)
is greater than 3 can be expressed as:

LENGTH[4] ∨ DEPTH [3];

3)  The Automatic Strategy Selection.

A very simple procedure is used to select the strategies in PROVE-mode.
The choice strategies are ANCESTRY and, if THEOREMNAME is present as an axiom name
,then SUPPORT[<value of THEOREMNAME>] is also used.  Also, if an equality predicate
letter is declared, then equality replacement witha  depth bound of 4 is added.

The editing strategies are determined by the maximum lengths and depths which occur in the 
input clauses.  If equality is present then a simplification list consisting of all the
positive units is used.

The strategy settings are automatically changed if the program is terminated without
finding a proof.
.NEXT PAGE 
IX. Theorem proving primitives.

It is now possible to write LISP-like programs which control the actions
of the theorem prover and manipulate clauses.  Data types  for CLAUSES,
STRATEGIES, and PATTERNS have been added to LISP so that the user can
describe his clause manipulations in the same notation which is used
to drive the on-line prover.  LISP functions, TRYTIL and FIND, have
been defined to perform controlled proof-attempts and clause-list searching.

1. Data Types.

a) [CLAUSES <clauses>] is used to introduce new clause lists to the program.
For example: (SETQ X [CLAUSES DSK:FOO])  when executed will assign to X the
clauselist manufactured from the statements on file FOO.

b) [CHOICE <strategy>] and [EDIT <strategy>] introduce the appropriate
strategies.

c) [PATTERN <pattern>] is useful in conjunction with FIND to filter out  clauses
which match <pattern>.


2. Procedures.

(TRYTIL <clauses><choice-strategy><edit-strategy><termination condition>)

where:
1) <clauses> is a list of clauses .
2) <choice-strategy> is a representation of a choice strategy.
3) <edit-strategy> represents an editing strategy.
4) <termination condition> is a functional argument which will be evaluated
periodically during the execution of the TRYTIL.  As long as the condition
evaluated to NIL the proof attempt will continue. If the condition becomes true
then TRYTIL will return the list of all deductions which have been made.

For example:

(TRYTIL [CLAUSES DSK: FOO] [CHOICE ANCESTRY∧SUPPORT[THEOREM]]
[EDIT LENGTH[4]∨DEPTH[3]] (FUNCTION (LAMBDA()(GREATERP LEVEL 3))) )

will begin a proof search using file DSK:FOO with choice strategy being AFF and
supporting the negation of the theorem.  Deductions whose length is greater than
4 or whose depth of fuction nesting is greater than 3 will be discarded.
The proof search will terminate at the end of level 3.

If a refutation is discovered during any attempt, (QED) is returned. If no refutation
is found, then the on-line editor is called to give the user a chance to examine
the current proof environment. There is a third way to exit TRYTIL: since
the on-line editor is available inside the proof attempt, typing ABandon <clauses>
to the  editor will force termination of the proof attempt and will return the 
selected <clauses>.


(FIND <clauses><pattern>)

where: 
1) <clauses> is a list of clauses.
2) <pattern> is a condition which is to be applied to each element of <clauses>.

The value of FIND is a list of all elements of <clauses> which satisfy the
<pattern>.



.END
.NEXT PAGE
.REQUIRE "ANSWER.PUB" SOURCE_FILE
.NEXT PAGE

.BEGIN DOUBLE SPACE
		APPENDIX

THE SYNTAX EQUATIONS FOR THE THEOREM PROVER.

The parsers for the input syntax and the command language are both contstructed
by Lynn Quam's
Syntax Directed Input Output program.


.END

THE INPUT FORMAT
.BEGIN DOUBLE SPACE
The usual form for input consists of the declarations of the non-logical
constituents of the axioms, followed by a sequence of statements.  The statements
may be assigned names, and if a statement whose name 
is the same as the current value of THEOREMNAME is present that statement
is negated before being added to the memory of the prover.
.END
.BEGIN VERBATIM
<INPUT>	::=<DECOP>:<OPLIST>;
	::=<ID>:
	::=<S>

<DECOP>	::=VAR | INF_OP | INF_PRED | PRE_OP | PRE_PRED | EQUALITY

<OPLIST>::=<OP>,<OPLIST>
	::=<OP>

<S>	::=;
	::=<S1>;

<S1>	::=<S2>
	::=<S1><EQUIV><S2>

<S2>	::=<S3>
	::=<S2><IMP><S3>

<S3>	::=<S4>
	::=<S3><OR><S4>

<S4>	::=<S5>
	::=<S4><AND><S5>

<S5>	::=(<S1>)
	::=<NOT><S5>
	::=<QFF><BODY>
	::=<PRED>

<BODY>	::= <IVAR><S5>
	::=(<VARLIST>)<S5>

<VARLIST>::=<IVAR>,<VARLIST>
	::=<IVAR>
.END

.BEGIN DOUBLE SPACE

In the following,the routines corresponding to <PREPREDLET>, <INFPREDLET>, <IVAR>, <PREFN>, and
<INFN> check the lists of prefix- and infix- predicate and function letters, and
the variable list, all of which were manufactured by the appropriate declarations.

.END

.BEGIN VERBATIM

<PRED>  ::=<PREPREDLET><ITMLST>
	::=<TM><INFPREDLET><TM>

<ITMLST>::=(<ITMS>)

<ITMS>  ::=<TM>,<ITMS>
	::=<TM>

<TM>    ::=<IVAR>
	::=<PREFN><ITMLST>
	::=<PREFN>
	::=(<TM>)
	::=<TM><INFN><TM>


The logical connectives are defined as follows:

<EQUIV>	::= ≡ | ↔ 

<IMP>	::= ⊃

<OR>	::= ∨

<AND>	::= ∧

<NOT>	::= ¬

<QFF>	::= ∀ | ∃
.END

.NEXT PAGE
THE SIMPLE STRATEGY LANGUAGE
.BEGIN DOUBLE SPACE

The most straightforwrd application of the strategy language consists
of using Boolean combinations of the builtin strategies. 
.END
.BEGIN VERBATIM

<STRATEGY>::=<F1>;

<F1>	::=<F2>
	::=<F1><OR><F2>

<F2>	::=<F3>
        ::=<F2><AND><F3>

<F3>	::=(<F1>)
	::=<NOT><F3>
	::=<PREDIC>

<PREDIC>::=ANCESTRY
	::=NONE
	::=VINE
	::=UNIT
	::=P1
	::=SUPPORT[<C>]
	::=MODEL[<PREDLST>;<PREDLST>]
	::=EQUALITY[<OP>;<NUMBER>]
	::=DEMOD[<CLAUSES><NUMBER>]
	::=DEFMODEL[ID]
	::=LENGTH[<NUMBER>]
	::=DEPTH[<NUMBER>]
	::=SELDEPTH[<FNLST>]
	::=<MPRM>

<PREDLST>
	::=<ID>,<PREDLST>
	::=<ID>
	::=

<FNLST>	::= <FP>;<FNLST>
	::= <FP>

<FP>	::=<OP>,<NUMBER>

.END

.NEXT PAGE
.BEGIN VERBATIM

THE COMMAND LANGUAGE


<CLAUSES> ::= <C>,<CLAUSES>
	::= <C>

<C>	::= @<S>
	::= DSK: <FILE>
	::= <NUMBER>
	::= <ID>[<VARLIST>]
	::= <ID>
	::= FIND [<ID>,<MATCH>]
	::= FINDC [<MATCH>]

<FILE>	::= <ID>
	::= (<ID>.<ID>)

<VARLIST> ::= <NUMBER>,<VARLIST>
	::= <NUMBER>

<COMMAND ::= AB <CLAUSES>;
	::= AB;
	::= AN <CLAUSES>;

	::= CH;
	::= CL <ID>;
	::= CU;

	::= DE <CLAUSES>;
	::= DI <CLAUSES>;
	::= DO <NUMBER>;
	::= DS <FILE>;

	::= EO;
	::= EV;
	::= EX;

	::= FD;
	::= FU;

	::= GO <NUMBER>;
	::= HA;
	::= HE;

	::= IN <ID> <CLAUSES>;

	::= ME <CLAUSES>;<CLAUSES>;

	::= PA <CLAUSES>;CLAUSES>;
	::= PR <CLAUSES>;

	::= RE <CLAUSES>;<CLAUSES>;

	::= SA <CLAUSES>;
	::= SE <ID> <CLAUSES>;
	::= SI <CLAUSES>; BY <CLAUSES>;
	::= SU <TM> FOR <TM> IN <CLAUSES>;
	::= SY;

	::= TE <CLAUSES>;
	::= TE;

	::= UP <NUMBER>;

.END
.NEXT PAGE

THE MATCHER

.BEGIN VERBATIM

<MATCH>	::= <M2>
	::=<MATCH> ∨ <M2>

<M2> 	::= <M3>
	::= <M2> ∧ <M3>

<M3> 	::= (<F1>)
	::=¬<M3>
	::=<MPRM>

<MPRM>	::= <ARG><MOP><ARG1>

	::= OCR[<PAT>]
	::=TREE[<CNAME>]

<MOP> 	::= =
	::= <
	::= >

<ARG1> ::= <ARG>

<ARG> 	::= LENGTH
	::=DEPTH
	::=<NUMBER>

<CNAME>	::= <NUMBER>
	::= <ID>[<VARLIST>]
	::= <ID>

<PAT>	::= <NOT><PRED>
	::=<PRED>
	::=<TM>
	::=<FNLET>

.END